/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30



␈↓ α∧␈↓α␈↓ β%DESCRIBING RECURSIVE FUNCTIONS IN FIRST ORDER LOGIC

␈↓ α∧␈↓␈↓ αTAfter␈αall␈αthese␈αyears,␈α
it␈αturns␈αout␈αthat␈αfirst␈α
order␈αlogic␈αis␈αadequate␈αfor␈α
directly␈αrepresenting
␈↓ α∧␈↓Lisp-like␈α
recursive␈α
function␈αdefinitions.␈α
 Most␈α
of␈α
the␈αidea␈α
is␈α
present␈αin␈α
(Cartwright␈α
1976),␈α
but␈αit
␈↓ α∧␈↓has␈α
probably␈α
been␈αanticipated␈α
by␈α
others.␈α It␈α
also␈α
turns␈αout␈α
that␈α
some␈αof␈α
the␈α
methods␈α
of␈αproving
␈↓ α∧␈↓assertions␈αabout␈αsuch␈αfunctions,␈αe.g.␈αsubgoal␈αinduction␈αand␈αthe␈αinductive␈αassertion␈αmethod␈αcan␈αbe
␈↓ α∧␈↓expressed␈αas␈αaxiom␈αschemata.␈α Another␈αuseful␈αidea␈αmay␈αbe␈αthat␈αof␈αhigher␈αorder␈αaxiom␈αschemata
␈↓ α∧␈↓in first order logic.

␈↓ α∧␈↓␈↓ αTWe start with the Lisp ␈↓↓append␈↓ function.  The usual internal notation for its definition is

␈↓ α∧␈↓1)␈↓ αt␈α
(DE␈α
APPEND␈α
(U␈α
V)␈α
(COND␈α
((NULL␈αU)␈α
V)␈α
(T␈α
(CONS␈α
(CAR␈α
U)␈α
(APPEND␈α(CDR␈α
U)
␈↓ α∧␈↓V))))),

␈↓ α∧␈↓but we shall write it

␈↓ α∧␈↓2)␈↓ αt ␈↓↓u * v ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓,

␈↓ α∧␈↓using the infix * for ␈↓↓append␈↓ and the other conventions of a proposed Lisp publication language.

␈↓ α∧␈↓␈↓ αTWhen␈αwe␈αwrite␈αsuch␈αa␈αrecursive␈αfunction␈αdefinition,␈αwe␈αare␈αneed␈αnot␈αknow␈αfor␈αwhat␈αvalues
␈↓ α∧␈↓of␈αits␈αarguments,␈αthe␈αcomputation␈αwill␈αterminate.␈α We␈αshall␈αtake␈αthe␈α←␈αsymbol␈αas␈αmeaning␈αthat␈αwe
␈↓ α∧␈↓want the least fixed point of the corresponding functional equation.  To emphasize the point,

␈↓ α∧␈↓3)␈↓ αt ␈↓↓f x ← f x␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓4)␈↓ αt ␈↓↓f x ← 1 + f x␈↓

␈↓ α∧␈↓are␈α∞considered␈α∞perfectly␈α∂good␈α∞recursive␈α∞function␈α∞definitions,␈α∂both␈α∞yielding␈α∞the␈α∂totally␈α∞undefined
␈↓ α∧␈↓partial␈α∀function.␈α∀ (Note␈α∀our␈α∀convention␈α∃that␈α∀parentheses␈α∀can␈α∀be␈α∀omitted␈α∀for␈α∃functions␈α∀and
␈↓ α∧␈↓predicates␈α
of␈α
one␈α
argument).␈α
 The␈α
former␈α
has␈α
every␈α
partial␈α
function␈α
as␈α
a␈α
solution␈α
of␈α
the␈α
functional
␈↓ α∧␈↓equation and the second has only the totally undefined function.

␈↓ α∧␈↓␈↓ αTNevertheless,␈αCartwright␈αshowed␈αthat␈αwe␈αcan␈αreplace␈αany␈αrecursive␈αfunction␈αdefinition␈αby␈αa
␈↓ α∧␈↓sentence␈αof␈α
first␈αorder␈αlogic␈α
provided␈αthe␈αfunctions␈α
are␈αgiven␈αsuitable␈α
interpretation.␈α In␈α
the␈αcase
␈↓ α∧␈↓of ␈↓↓append,␈↓ we get

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀u v.(u * v = ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . [␈↓αd␈↓↓ u * v]␈↓.

␈↓ α∧␈↓and (4) becomes

␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀x.(f x = 1 + f x)␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α⊃equations␈α⊂are␈α⊃interpreted␈α⊃as␈α⊂follows:␈α⊃The␈α⊃domain␈α⊂of␈α⊃interest,␈α⊃the␈α⊂Lisp␈α⊃lists␈α⊃or␈α⊂the
␈↓ α∧␈↓integers␈α∞in␈α∞the␈α
above␈α∞cases,␈α∞is␈α∞considered␈α
as␈α∞imbedded␈α∞in␈α∞a␈α
larger␈α∞domain.␈α∞ The␈α∞larger␈α
domain


␈↓ α∧␈↓␈↓ ε|1␈↓ ∧



␈↓ α∧␈↓does␈αnot␈αneed␈α
to␈αbe␈αspecified,␈α
but␈αyou␈αmay␈α
imagine␈αit␈αto␈α
contain␈αonly␈αone␈α
element␈αbesides␈αthose␈α
in
␈↓ α∧␈↓the␈αlower␈αdomain␈α-␈αthe␈αundefined␈αelement␈α␈↓	W␈↓.␈α There␈αis␈αno␈αneed␈αto␈αsay␈αwhat␈αelements␈αit␈αcontains,
␈↓ α∧␈↓because␈α
the␈α
proofs␈α
in␈α∞the␈α
language␈α
don't␈α
depend␈α
on␈α∞it.␈α
 The␈α
quantifiers␈α
using␈α
lower␈α∞case␈α
letters
␈↓ α∧␈↓are␈αover␈αthe␈αinner␈αdomain␈α
-␈αLisp␈αlists␈αor␈αintegers.␈α
 However,␈αthe␈αvalues␈αof␈αthe␈αrecursively␈α
defined
␈↓ α∧␈↓functions␈αare␈αnot␈α␈↓↓a␈α
priori␈↓␈αconsidered␈αto␈αbe␈αin␈α
the␈αinner␈αdomain.␈α In␈αthe␈α
case␈αof␈α␈↓↓append,␈↓␈αit␈αwill␈α
be
␈↓ α∧␈↓proved␈αfrom␈αsuitable␈αLisp␈αaxioms␈αthat␈α␈↓↓u␈α*␈αv␈↓␈αis␈αa␈αlist,␈αand␈αit␈αfollows␈αfrom␈αsuitable␈αinteger␈αaxioms
␈↓ α∧␈↓that ␈↓↓g(x)␈↓ is never an integer.

␈↓ α∧␈↓What␈α
allows␈αus␈α
to␈αwrite␈α
the␈αequations␈α
is␈α
the␈αinterpretation␈α
that␈αthe␈α
equation␈αcan␈α
be␈α
satisfied␈αby
␈↓ α∧␈↓the␈α∞least␈α
fixed␈α∞point␈α∞taken␈α
in␈α∞the␈α
Scott␈α∞sense.␈α∞ Thus␈α
␈↓↓append␈↓␈α∞can␈α
be␈α∞taken␈α∞to␈α
be␈α∞the␈α∞least␈α
fixed
␈↓ α∧␈↓point of the second order functional

␈↓ α∧␈↓7)␈↓ αt ␈↓↓F = λf.λu v.[␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αa␈↓↓ u . f[␈↓αd␈↓↓ u, v]]␈↓.

␈↓ α∧␈↓According to the Scott theory, the fixed point will indeed satisfy (5).

␈↓ α∧␈↓␈↓ αTCartwright␈α
used␈α
this␈α
characterization␈α
of␈α
recursive␈α
functions␈α
to␈α
prove␈α
facts␈α
about␈α
them␈αin␈α
his
␈↓ α∧␈↓human␈α∂aided␈α∂first␈α∂order␈α∂theorem␈α∂prover.␈α∂ His␈α∞paper␈α∂is␈α∂also␈α∂based␈α∂on␈α∂a␈α∂method␈α∂of␈α∞recursively
␈↓ α∧␈↓defining␈α∞data␈α∞structures␈α∞which␈α∂he␈α∞calls␈α∞␈↓↓typed␈α∞Lisp␈↓.␈α∞ In␈α∂this␈α∞note,␈α∞however,␈α∞we␈α∞are␈α∂interested␈α∞in
␈↓ α∧␈↓pursuing the methods of description, and this is as far as Cartwright takes us in this direction.

␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Artificial Intelligence Laboratory
␈↓ α∧␈↓Computer Science Department
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305

␈↓ α∧␈↓ARPANET: MCCARTHY@SU-AI

␈↓ α∧␈↓␈↓εThis draft of

␈↓ α∧␈↓εPUBbed at 16:51 on January 27, 1977.␈↓

















␈↓ α∧␈↓␈↓ ε|2␈↓ ∧